A:Type, eq:EqDecider(A), B:(AType), P:(A), f:x:A fp B(x), a:A.
a  dom(f)  (b:A. P(b)  b = a)  fpf-vals(eq;P;f) = [<a,f(a)>]  (x:AB(x)) List 

latex

Definitions

a:A fp B(a), let x = a in b(x), fpf-vals(eq;P;f), t  T, x:A. B(x), EqDecider(T), , x(s), x. t(x), Top, x  dom(f), b, Prop, P  Q, P  Q, remove-repeats(eq;L), no_repeats(T;l), (x  l), P & Q, P  Q, filter(P;l), deq-member(eq;x;L), if b t else f fi, P  Q, A, b, Unit, False, {T}, SQType(T), S  T, ||as||, ij, hd(l), AB, tl(l), i<j, ij, nth_tl(n;as), l[i], Y, , f(x), map(f;as), zip(as;bs)

Lemmas

ge wf, tl wf, hd wf, non neg length, length wf1, member wf, bool cases, bool sq, remove-repeats wf, nil member, false wf, cons member, no repeats wf, no repeats cons, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, deq-member wf, bnot wf, not wf, l member wf, assert-deq-member, remove-repeats property, iff wf, assert wf, fpf-dom wf, fpf-trivial-subtype-top, fpf wf, bool wf, deq wf